package com.googlecode.kipler.satisfiability.completion.rule.individual;

import java.util.Iterator;
import java.util.Set;

import com.googlecode.kipler.container.dl.ABox;
import com.googlecode.kipler.container.dl.ConceptCategory;
import com.googlecode.kipler.container.dl.Individual;
import com.googlecode.kipler.container.dl.operational.FilterType;
import com.googlecode.kipler.container.dl.operational.RelatedIndividualWithTypeFilterFactory;
import com.googlecode.kipler.satisfiability.blocking.abox.ABoxBlockingStrategy;
import com.googlecode.kipler.satisfiability.clash.ClashDetectionStrategy;
import com.googlecode.kipler.satisfiability.clash.InstantQNRClashDetectionStrategy;
import com.googlecode.kipler.satisfiability.completion.branching.IdentificationBranchingPoint;
import com.googlecode.kipler.satisfiability.reasoner.BranchingException;
import com.googlecode.kipler.satisfiability.reasoner.Reasoner;
import com.googlecode.kipler.satisfiability.reasoner.ReasonerException;
import com.googlecode.kipler.satisfiability.reasoner.UnsatisfiableException;
import com.googlecode.kipler.syntax.concept.Concept;
import com.googlecode.kipler.syntax.concept.QualifiedNoRestriction;
import com.googlecode.kipler.syntax.formula.ConceptAssertion;


/**
 * 
 * @author İnanç Seylan
 * 
 */
public class AtMostRule extends ABoxRule {
	private ABox aBox;

	private boolean applied;

	private Reasoner prover;

	private ABoxBlockingStrategy blocking;

	private MergeStrategy mergeStrategy;

	public AtMostRule(Reasoner prover, ABoxBlockingStrategy blocking,
			MergeStrategy mergeStrategy) {
		this.prover = prover;
		setBlocking(blocking);
		setMergeStrategy(mergeStrategy);
	}

	public ABoxBlockingStrategy getBlocking() {
		return blocking;
	}

	public void setBlocking(ABoxBlockingStrategy blocking) {
		this.blocking = blocking;
	}

	public MergeStrategy getMergeStrategy() {
		return mergeStrategy;
	}

	public void setMergeStrategy(MergeStrategy mergeStrategy) {
		this.mergeStrategy = mergeStrategy;
	}

	public boolean isApplied() {
		return applied;
	}

	@Override
	public void apply() throws ReasonerException {
		applied = false;
		aBox = getWorld().getABox();
		if (!getBlocking().isIndirectlyBlocked(aBox, getIndividual().getName())) {
			for (Iterator<Concept> i = getIndividual().conceptIterator(
					ConceptCategory.AT_MOST); i.hasNext();) {
				Concept concept = i.next();
				QualifiedNoRestriction qr = (QualifiedNoRestriction) concept;
				Set<Individual> neighbors = RelatedIndividualWithTypeFilterFactory
						.getFilter(FilterType.TYPED_NEIGHBOR, aBox,
								getIndividual(), qr.getRole(), qr.getConcept())
						.filter();
				if (neighbors.size() > qr.getNo()) {
					ClashDetectionStrategy clashStrategy = new InstantQNRClashDetectionStrategy(
							neighbors);
					if (clashStrategy.hasClash(aBox, new ConceptAssertion(qr,
							getIndividual().getName()))) {
						throw new UnsatisfiableException(clashStrategy
								.getDependencySet(), clashStrategy
								.getExplanation());
					}
					MergePair mergePair = getMergeStrategy().choosePair(aBox,
							neighbors);
					/*
					 * Since there may be more than one instance of this rule in
					 * the same completion strategy for different merge
					 * strategies, we must check whether a merge pair has been
					 * found for this merge strategy.
					 */
					if (!mergePair.equals(MergePair.emptyPair())) {
						IdentificationBranchingPoint bp = new IdentificationBranchingPoint();
						bp.setWcs(getWcs());
						bp.setWorld(getWorld());
						bp.setIndividual(getIndividual());
						bp.setMergePair(mergePair);
						bp.setMergeStrategy(getMergeStrategy());
						applied = true;
						prover.addBranch(bp);
						throw new BranchingException();
					}
				}
			}
		}
	}
}
